Strongest postcondition semantics as the formal basis for reverse engineering
Identifieur interne : 00C020 ( Main/Exploration ); précédent : 00C019; suivant : 00C021Strongest postcondition semantics as the formal basis for reverse engineering
Auteurs : Gerald C. Gannod [États-Unis] ; Betty H. C. Cheng [États-Unis]Source :
- Automated Software Engineering [ 0928-8910 ] ; 1996-06-01.
English descriptors
- KwdEn :
- Teeft :
- Actual parameters, Alternation, Alternation statement, Alternation statements, Assignment statement, Assignment statements, Cheng, Chikofsky, Code sequence, Conjunct, Correctness, Dijkstra, Final value, Formal basis, Formal methods, Formal semantics, Formal specification, Formal specifications, Free occurrences, Gannod, Gries, Historical subscripts, Hoare, Ieee, Initial value, Initial values, Iteration, Iteration statement, Local variables, Notation, Numtwo0, Pages ieee, Partial correctness model, Postcondition, Precondition, Predicate, Predicate transformer, Predicate transformers, Procedure body, Procedure declaration, Program code, Program semantics, Scholten, Semantics, Software, Software development, Software engineering, Software maintenance, Specification, Strongest postcondition, Strongest postcondition predicate transformer, Strongest postcondition semantics, Subscript, Substitution, Swapb, Temp, Textual, Textual substitution, Total correctness model, Transformer, Weakest precondition predicate transformer.
Abstract
Abstract: Reverse engineering of program code is the process of constructing a higher level abstraction of an implementation in order to facilitate the understanding of a system that may be in a “legacy” or “geriatric” state. Changing architectures and improvements in programming methods, including formal methods in software development and object-oriented programming, have prompted a need to reverse engineer and re-engineer program code. This paper describes the application of the strongest postcondition predicate transformer (sp) as the formal basis for the reverse engineering of imperative program code.
Url:
DOI: 10.1007/BF00126962
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000F00
- to stream Istex, to step Curation: 000E87
- to stream Istex, to step Checkpoint: 002921
- to stream Main, to step Merge: 00C841
- to stream Main, to step Curation: 00C020
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Strongest postcondition semantics as the formal basis for reverse engineering</title><author><name sortKey="Gannod, Gerald C" sort="Gannod, Gerald C" uniqKey="Gannod G" first="Gerald C." last="Gannod">Gerald C. Gannod</name></author><author><name sortKey="Cheng, Betty H C" sort="Cheng, Betty H C" uniqKey="Cheng B" first="Betty H. C." last="Cheng">Betty H. C. Cheng</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:3F88A804BBC4B42878FB1D76BFA6316DC6F1BDD3</idno><date when="1996" year="1996">1996</date><idno type="doi">10.1007/BF00126962</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-Z3GN0P49-C/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000F00</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000F00</idno><idno type="wicri:Area/Istex/Curation">000E87</idno><idno type="wicri:Area/Istex/Checkpoint">002921</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002921</idno><idno type="wicri:doubleKey">0928-8910:1996:Gannod G:strongest:postcondition:semantics</idno><idno type="wicri:Area/Main/Merge">00C841</idno><idno type="wicri:Area/Main/Curation">00C020</idno><idno type="wicri:Area/Main/Exploration">00C020</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Strongest postcondition semantics as the formal basis for reverse engineering</title><author><name sortKey="Gannod, Gerald C" sort="Gannod, Gerald C" uniqKey="Gannod G" first="Gerald C." last="Gannod">Gerald C. Gannod</name><affiliation wicri:level="4"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Department of Computer Science, Michigan State University, 48824-1027, East Lansing, Michigan</wicri:regionArea><placeName><region type="state">Michigan</region><settlement type="city">East Lansing</settlement></placeName><orgName type="university">Université d'État du Michigan</orgName></affiliation></author><author><name sortKey="Cheng, Betty H C" sort="Cheng, Betty H C" uniqKey="Cheng B" first="Betty H. C." last="Cheng">Betty H. C. Cheng</name><affiliation wicri:level="4"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Department of Computer Science, Michigan State University, 48824-1027, East Lansing, Michigan</wicri:regionArea><placeName><region type="state">Michigan</region><settlement type="city">East Lansing</settlement></placeName><orgName type="university">Université d'État du Michigan</orgName></affiliation></author></analytic><monogr></monogr><series><title level="j">Automated Software Engineering</title><title level="j" type="sub">An International Journal</title><title level="j" type="abbrev">Automated Software Engineering</title><idno type="ISSN">0928-8910</idno><idno type="eISSN">1573-7535</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="1996-06-01">1996-06-01</date><biblScope unit="volume">3</biblScope><biblScope unit="issue">1-2</biblScope><biblScope unit="page" from="139">139</biblScope><biblScope unit="page" to="164">164</biblScope></imprint><idno type="ISSN">0928-8910</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0928-8910</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>formal methods</term><term>formal specification</term><term>reverse engineering</term><term>software maintenance</term></keywords><keywords scheme="Teeft" xml:lang="en"><term>Actual parameters</term><term>Alternation</term><term>Alternation statement</term><term>Alternation statements</term><term>Assignment statement</term><term>Assignment statements</term><term>Cheng</term><term>Chikofsky</term><term>Code sequence</term><term>Conjunct</term><term>Correctness</term><term>Dijkstra</term><term>Final value</term><term>Formal basis</term><term>Formal methods</term><term>Formal semantics</term><term>Formal specification</term><term>Formal specifications</term><term>Free occurrences</term><term>Gannod</term><term>Gries</term><term>Historical subscripts</term><term>Hoare</term><term>Ieee</term><term>Initial value</term><term>Initial values</term><term>Iteration</term><term>Iteration statement</term><term>Local variables</term><term>Notation</term><term>Numtwo0</term><term>Pages ieee</term><term>Partial correctness model</term><term>Postcondition</term><term>Precondition</term><term>Predicate</term><term>Predicate transformer</term><term>Predicate transformers</term><term>Procedure body</term><term>Procedure declaration</term><term>Program code</term><term>Program semantics</term><term>Scholten</term><term>Semantics</term><term>Software</term><term>Software development</term><term>Software engineering</term><term>Software maintenance</term><term>Specification</term><term>Strongest postcondition</term><term>Strongest postcondition predicate transformer</term><term>Strongest postcondition semantics</term><term>Subscript</term><term>Substitution</term><term>Swapb</term><term>Temp</term><term>Textual</term><term>Textual substitution</term><term>Total correctness model</term><term>Transformer</term><term>Weakest precondition predicate transformer</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Reverse engineering of program code is the process of constructing a higher level abstraction of an implementation in order to facilitate the understanding of a system that may be in a “legacy” or “geriatric” state. Changing architectures and improvements in programming methods, including formal methods in software development and object-oriented programming, have prompted a need to reverse engineer and re-engineer program code. This paper describes the application of the strongest postcondition predicate transformer (sp) as the formal basis for the reverse engineering of imperative program code.</div></front></TEI><affiliations><list><country><li>États-Unis</li></country><region><li>Michigan</li></region><settlement><li>East Lansing</li></settlement><orgName><li>Université d'État du Michigan</li></orgName></list><tree><country name="États-Unis"><region name="Michigan"><name sortKey="Gannod, Gerald C" sort="Gannod, Gerald C" uniqKey="Gannod G" first="Gerald C." last="Gannod">Gerald C. Gannod</name></region><name sortKey="Cheng, Betty H C" sort="Cheng, Betty H C" uniqKey="Cheng B" first="Betty H. C." last="Cheng">Betty H. C. Cheng</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00C020 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00C020 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:3F88A804BBC4B42878FB1D76BFA6316DC6F1BDD3
|texte= Strongest postcondition semantics as the formal basis for reverse engineering
}}
| This area was generated with Dilib version V0.6.33. |  |